Inference at * 2 0 1 1 
Iof proof for Lemma multiply nat wf:

.....downcase..... NILNIL

1. i : 
2. j : 
3. j < 0
4. ((j+1)  0 )  (0  (i * (j+1)))
  (j  0 )  (0  (i * j)) 

latex

 by D 0 

latex

 1: 

 1: 5. j  0 
 1:   0  (i * j)
 2: .....wf..... NILNIL

 2:   (j  0 )  
 .

Definitions	Type, s = t, n * m, n+m, #$n, a < b, , , A  B, x:AB(x), i  j , P  Q, t  T,
Lemmas	le wf, ge wf